ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple(ds; da).
ecl-trans-normal(v)  prop{i:l} 

latex

Definitions	t  T, , x:A. B(x), no_repeats(T; l), P  Q, sorted(L), P  Q, prop{i:l}, finite-type(T), b, A, , decidable(P), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-normal(x), ecl-trans-tuple{i:l}(ds; da), Id, x. t(x), fpf(A; a.B(a)), Knd
Lemmas	ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable wf, nat wf, not wf, assert wf, finite-type wf, sorted wf, no repeats wf, nat plus wf